(0) Obligation:

Runtime Complexity TRS:
The TRS R consists of the following rules:

0(0(1(x1))) → 0(1(2(0(x1))))
0(0(1(x1))) → 0(3(1(0(x1))))
0(0(1(x1))) → 1(0(4(0(x1))))
0(0(1(x1))) → 0(1(3(0(2(x1)))))
0(0(1(x1))) → 0(1(3(0(4(x1)))))
0(0(1(x1))) → 0(2(0(1(2(x1)))))
0(0(1(x1))) → 0(3(0(1(2(x1)))))
0(0(1(x1))) → 0(3(0(3(1(x1)))))
0(0(1(x1))) → 0(4(0(4(1(x1)))))
0(0(1(x1))) → 1(2(0(2(0(x1)))))
0(0(1(x1))) → 1(2(2(0(0(x1)))))
0(0(1(x1))) → 0(0(2(2(1(2(x1))))))
0(0(1(x1))) → 0(1(2(4(2(0(x1))))))
0(0(1(x1))) → 1(2(0(3(0(4(x1))))))
0(1(1(x1))) → 0(2(1(1(x1))))
0(1(1(x1))) → 0(3(1(1(x1))))
0(1(1(x1))) → 1(1(3(0(4(x1)))))
0(1(1(x1))) → 1(2(0(2(1(x1)))))
0(1(1(x1))) → 1(0(3(1(2(4(x1))))))
0(1(1(x1))) → 1(0(4(2(1(2(x1))))))
0(1(1(x1))) → 1(1(2(4(3(0(x1))))))
0(1(1(x1))) → 1(2(1(0(4(4(x1))))))
0(1(1(x1))) → 1(2(2(1(3(0(x1))))))
0(5(1(x1))) → 0(3(1(5(x1))))
0(5(1(x1))) → 0(4(5(1(x1))))
0(5(1(x1))) → 0(2(3(1(5(x1)))))
0(5(1(x1))) → 0(3(1(5(2(x1)))))
0(5(1(x1))) → 0(3(1(2(5(2(x1))))))
5(0(1(x1))) → 5(1(2(4(0(x1)))))
5(0(1(x1))) → 5(0(2(1(2(4(x1))))))
5(0(1(x1))) → 5(1(2(3(0(4(x1))))))
0(0(1(5(x1)))) → 0(4(1(0(5(x1)))))
0(0(2(1(x1)))) → 2(0(3(0(2(1(x1))))))
0(0(2(1(x1)))) → 2(3(0(2(0(1(x1))))))
0(1(0(1(x1)))) → 1(0(2(0(1(x1)))))
0(1(1(1(x1)))) → 1(1(3(1(0(x1)))))
5(0(1(1(x1)))) → 1(5(1(2(0(x1)))))
5(3(0(1(x1)))) → 5(1(2(3(0(x1)))))
5(3(1(5(x1)))) → 5(3(1(2(5(x1)))))
5(3(2(1(x1)))) → 1(2(3(5(2(x1)))))
5(4(0(1(x1)))) → 1(2(5(0(4(x1)))))
0(0(5(1(5(x1))))) → 1(2(5(5(0(0(x1))))))
0(5(3(0(1(x1))))) → 1(0(5(3(0(4(x1))))))
0(5(3(4(1(x1))))) → 1(0(3(5(4(5(x1))))))
0(5(4(0(1(x1))))) → 0(1(3(0(4(5(x1))))))
5(4(2(1(1(x1))))) → 5(4(1(2(1(2(x1))))))

Rewrite Strategy: INNERMOST

(1) CpxTrsMatchBoundsProof (EQUIVALENT transformation)

A linear upper bound on the runtime complexity of the TRS R could be shown with a Match Bound [MATCHBOUNDS1,MATCHBOUNDS2] of 1.
The certificate found is represented by the following graph.
Start state: 3782
Accept states: [3783, 3784]
Transitions:
3782→3783[0_1|0]
3782→3784[5_1|0]
3782→3782[1_1|0, 2_1|0, 3_1|0, 4_1|0]
3782→3785[1_1|1]
3782→3788[1_1|1]
3782→3791[4_1|1]
3782→3795[1_1|1]
3782→3799[4_1|1]
3782→3804[2_1|1]
3782→3809[0_1|1]
3782→3814[4_1|1]
3782→3819[0_1|1]
3782→3824[0_1|1]
3782→3828[2_1|1]
3782→3833[2_1|1]
3785→3786[1_1|1]
3786→3787[2_1|1]
3787→3783[0_1|1]
3787→3809[0_1|1]
3787→3819[0_1|1]
3787→3824[0_1|1]
3788→3789[1_1|1]
3789→3790[3_1|1]
3790→3783[0_1|1]
3790→3809[0_1|1]
3790→3819[0_1|1]
3790→3824[0_1|1]
3791→3792[0_1|1]
3792→3793[3_1|1]
3793→3794[1_1|1]
3794→3783[1_1|1]
3794→3809[1_1|1]
3794→3819[1_1|1]
3794→3824[1_1|1]
3795→3796[2_1|1]
3796→3797[0_1|1]
3797→3798[2_1|1]
3798→3783[1_1|1]
3798→3809[1_1|1]
3798→3819[1_1|1]
3798→3824[1_1|1]
3799→3800[2_1|1]
3800→3801[1_1|1]
3801→3802[3_1|1]
3802→3803[0_1|1]
3803→3783[1_1|1]
3803→3809[1_1|1]
3803→3819[1_1|1]
3803→3824[1_1|1]
3804→3805[1_1|1]
3805→3806[2_1|1]
3806→3807[4_1|1]
3807→3808[0_1|1]
3808→3783[1_1|1]
3808→3809[1_1|1]
3808→3819[1_1|1]
3808→3824[1_1|1]
3809→3810[3_1|1]
3810→3811[4_1|1]
3811→3812[2_1|1]
3812→3813[1_1|1]
3813→3783[1_1|1]
3813→3809[1_1|1]
3813→3819[1_1|1]
3813→3824[1_1|1]
3814→3815[4_1|1]
3815→3816[0_1|1]
3816→3817[1_1|1]
3817→3818[2_1|1]
3818→3783[1_1|1]
3818→3809[1_1|1]
3818→3819[1_1|1]
3818→3824[1_1|1]
3819→3820[3_1|1]
3820→3821[1_1|1]
3821→3822[2_1|1]
3822→3823[2_1|1]
3823→3783[1_1|1]
3823→3809[1_1|1]
3823→3819[1_1|1]
3823→3824[1_1|1]
3824→3825[1_1|1]
3825→3826[3_1|1]
3826→3827[1_1|1]
3827→3783[1_1|1]
3827→3809[1_1|1]
3827→3819[1_1|1]
3827→3824[1_1|1]
3828→3829[1_1|1]
3829→3830[2_1|1]
3830→3831[1_1|1]
3831→3832[4_1|1]
3832→3784[5_1|1]
3833→3834[5_1|1]
3834→3835[3_1|1]
3835→3836[2_1|1]
3836→3784[1_1|1]

(2) BOUNDS(O(1), O(n^1))